DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2011.233

System T and the Product of Selection Functions

Authors: Martin Escardo, Paulo Oliva, and Thomas Powell

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract

We show that the finite product of selection functions (for all finite types) is primitive recursively equivalent to Goedel's higher-type recursor (for all finite types). The correspondence is shown to hold for similar restricted fragments of both systems: The recursor for type level n+1 is primitive recursively equivalent to the finite product of selection functions of type level n. Whereas the recursor directly interprets induction, we show that other classical arithmetical principles such as bounded collection and finite choice are more naturally interpreted via the product of selection functions.

Cite as

Martin Escardo, Paulo Oliva, and Thomas Powell. System T and the Product of Selection Functions. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 233-247, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{escardo_et_al:LIPIcs.CSL.2011.233,
  author =	{Escardo, Martin and Oliva, Paulo and Powell, Thomas},
  title =	{{System T and the Product of Selection Functions}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{233--247},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.233},
  URN =		{urn:nbn:de:0030-drops-32341},
  doi =		{10.4230/LIPIcs.CSL.2011.233},
  annote =	{Keywords: primitive recursion, product of selection functions, finite choice, dialectica interpretation}
}

Document

DOI: 10.4230/DagSemProc.05021.23

Unifying Functional Interpretations

Authors: Paulo Oliva

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)

Abstract

The purpose of this article is to present a parametrised functional interpretation. Depending on the choice of the two parameters one obtains well-known functional interpretations, among others GÃƒÂ¶del's Dialectica interpretation, Diller-Nahm's variant of the Dialectica interpretation, Kreisel's modified realizability, Kohlenbach's monotone interpretations and Stein's family of functional interpretations. We show that all these interpretations only differ on two basic choices, which are captured by the parameters, namely the choices of (1) "how much" of the counter-examples for A becomes witnesses for the negation of A, and of (2) "how much" information about the witnesses of A one is interested in.

Cite as

Paulo Oliva. Unifying Functional Interpretations. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{oliva:DagSemProc.05021.23,
  author =	{Oliva, Paulo},
  title =	{{Unifying Functional Interpretations}},
  booktitle =	{Mathematics, Algorithms, Proofs},
  pages =	{1--20},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5021},
  editor =	{Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.23},
  URN =		{urn:nbn:de:0030-drops-2919},
  doi =		{10.4230/DagSemProc.05021.23},
  annote =	{Keywords: Functional interpretation, modified realizability, Dialectica interpretation, intuitionistic logic}
}

Search Results

Documents authored by Oliva, Paulo

System T and the Product of Selection Functions

Abstract

Cite as

Unifying Functional Interpretations

Abstract

Cite as

Thanks for your feedback!

Could not send message